\begin{tabbing}
(\=(((((((Unfold `fseg` 0) \+
\\[0ex]CollapseTHEN (Auto'))$\cdot$) 
\\[0ex]CollapseTHEN (D ({-}1)$\cdot$))$\cdot$) 
\\[0ex]
\\[0ex]CollapseTHEN (ExRepD$\cdot$))$\cdot$) 
\\[0ex]CollapseTHEN (((WeakSubstFor $l_{2}$ 0) 
\\[0ex]CollapseTHEN ((((Assert 
\-\\[0ex]$\neg$\=($\uparrow$null($L$))) \+
\\[0ex]THENL [(((((((DVar `L') 
\\[0ex]CollapseTHEN (Reduce 0))$\cdot$) 
\\[0ex]CollapseTHEN (Auto$\cdot$
\-\\[0ex])\=)$\cdot$) \+
\\[0ex]CollapseTHEN (((((((if (first\_bool T:b) then HypSubst' else RevHypSubst') ( {-}3)( {-}2
\-\\[0ex]))$\cdot$) 
\\[0ex]T\=HENM (Reduce ({-}2)))$\cdot$) \+
\\[0ex]CollapseTHEN (Auto$\cdot$))$\cdot$))$\cdot$); Id]$\cdot$) 
\\[0ex]CollapseTHEN (((
\-\\[0ex]I\=nstLemma `last\_lemma` [$T$;$L$]) \+
\\[0ex]CollapseTHENA (Auto$\cdot$))$\cdot$))$\cdot$))$\cdot$))$\cdot$
\-
\end{tabbing}